:: ALGSPEC1 semantic presentation

theorem E1: :: ALGSPEC1:1
for b1, b2, b3 being Function holds
( (dom b1) /\ (dom b2) c= dom b3 implies (b1 +* b2) +* b3 = (b2 +* b1) +* b3 )
proof
let c1, c2, c3 be Function;
E2: dom ((c1 +* c2) +* c3) = (dom (c1 +* c2)) \/ (dom c3) by FUNCT_4:def 1;
E3: dom ((c2 +* c1) +* c3) = (dom (c2 +* c1)) \/ (dom c3) by FUNCT_4:def 1;
E4: ( dom (c1 +* c2) = (dom c1) \/ (dom c2) & dom (c2 +* c1) = (dom c2) \/ (dom c1) ) by FUNCT_4:def 1;
assume E5: (dom c1) /\ (dom c2) c= dom c3 ;
now
let c4 be set ;
assume E6: c4 in ((dom c1) \/ (dom c2)) \/ (dom c3) ;
per cases not ( not c4 in dom c3 & c4 in dom c3 ) ;
suppose c4 in dom c3 ;
then ( ((c1 +* c2) +* c3) . c4 = c3 . c4 & ((c2 +* c1) +* c3) . c4 = c3 . c4 ) by FUNCT_4:14;
hence ((c1 +* c2) +* c3) . c4 = ((c2 +* c1) +* c3) . c4 ;
end;
suppose E7: not c4 in dom c3 ;
then E8: ( c4 in (dom c2) \/ (dom c1) & not c4 in (dom c1) /\ (dom c2) ) by E5, E6, XBOOLE_0:def 2;
E9: ( ((c1 +* c2) +* c3) . c4 = (c1 +* c2) . c4 & ((c2 +* c1) +* c3) . c4 = (c2 +* c1) . c4 ) by E7, FUNCT_4:12;
( ( c4 in dom c1 or c4 in dom c2 ) & not ( c4 in dom c1 & c4 in dom c2 ) ) by E8, XBOOLE_0:def 2, XBOOLE_0:def 3;
then ( ( (c1 +* c2) . c4 = c1 . c4 & (c2 +* c1) . c4 = c1 . c4 ) or ( (c1 +* c2) . c4 = c2 . c4 & (c2 +* c1) . c4 = c2 . c4 ) ) by FUNCT_4:12, FUNCT_4:14;
hence ((c1 +* c2) +* c3) . c4 = ((c2 +* c1) +* c3) . c4 by E9;
end;
end;
end;
hence (c1 +* c2) +* c3 = (c2 +* c1) +* c3 by E2, E3, E4, FUNCT_1:9;
end;

theorem E2: :: ALGSPEC1:2
for b1, b2, b3 being Function holds
( ( b1 c= b2 & (rng b3) /\ (dom b2) c= dom b1 ) implies ( b2 * b3 = b1 * b3 ) )
proof
let c1, c2, c3 be Function;
assume E3: ( c1 c= c2 & (rng c3) /\ (dom c2) c= dom c1 ) ;
E4: dom (c1 * c3) = dom (c2 * c3)
proof
c1 * c3 c= c2 * c3 by E3, RELAT_1:48;
hence dom (c1 * c3) c= dom (c2 * c3) by RELAT_1:25; :: according to XBOOLE_0:def 10
let c4 be set ; :: according to TARSKI:def 3
assume c4 in dom (c2 * c3) ;
then E5: ( c4 in dom c3 & c3 . c4 in dom c2 ) by FUNCT_1:21;
then c3 . c4 in rng c3 by FUNCT_1:def 5;
then c3 . c4 in (rng c3) /\ (dom c2) by E5, XBOOLE_0:def 3;
hence c4 in dom (c1 * c3) by E3, E5, FUNCT_1:21;
end;
now
let c4 be set ;
assume c4 in dom (c1 * c3) ;
then E5: ( c4 in dom c3 & c3 . c4 in dom c1 & c3 . c4 in dom c2 ) by E4, FUNCT_1:21;
then ( c3 . c4 in rng c3 & (c2 * c3) . c4 = c2 . (c3 . c4) & (c1 * c3) . c4 = c1 . (c3 . c4) ) by FUNCT_1:23, FUNCT_1:def 5;
hence (c2 * c3) . c4 = (c1 * c3) . c4 by E3, E5, GRFUNC_1:8;
end;
hence c2 * c3 = c1 * c3 by E4, FUNCT_1:9;
end;

theorem E3: :: ALGSPEC1:3
for b1, b2, b3 being Function holds
( ( dom b1 c= rng b2 & dom b1 misses rng b3 & b2 .: (dom b3) misses dom b1 ) implies ( b1 * (b2 +* b3) = b1 * b2 ) )
proof
let c1, c2, c3 be Function;
assume E4: ( dom c1 c= rng c2 & dom c1 misses rng c3 & c2 .: (dom c3) misses dom c1 ) ;
E5: dom (c1 * c2) = dom (c1 * (c2 +* c3))
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10
let c4 be set ;
assume c4 in dom (c1 * c2) ;
then E6: ( c4 in dom c2 & c2 . c4 in dom c1 ) by FUNCT_1:21;
now
assume c4 in dom c3 ;
then c2 . c4 in c2 .: (dom c3) by E6, FUNCT_1:def 12;
hence not verum by E4, E6, XBOOLE_0:3;
end;
then ( c4 in dom (c2 +* c3) & c2 . c4 = (c2 +* c3) . c4 ) by E6, FUNCT_4:12, FUNCT_4:13;
hence c4 in dom (c1 * (c2 +* c3)) by E6, FUNCT_1:21;
end;
let c4 be set ; :: according to TARSKI:def 3
assume c4 in dom (c1 * (c2 +* c3)) ;
then E6: ( c4 in dom (c2 +* c3) & (c2 +* c3) . c4 in dom c1 ) by FUNCT_1:21;
then ( ( c4 in dom c2 & not c4 in dom c3 ) or c4 in dom c3 ) by FUNCT_4:13;
then ( ( c4 in dom c2 & (c2 +* c3) . c4 = c2 . c4 ) or ( (c2 +* c3) . c4 = c3 . c4 & c3 . c4 in rng c3 ) ) by FUNCT_1:def 5, FUNCT_4:12, FUNCT_4:14;
hence c4 in dom (c1 * c2) by E4, E6, FUNCT_1:21, XBOOLE_0:3;
end;
now
let c4 be set ;
assume c4 in dom (c1 * c2) ;
then E6: ( c4 in dom c2 & c2 . c4 in dom c1 ) by FUNCT_1:21;
now
assume c4 in dom c3 ;
then c2 . c4 in c2 .: (dom c3) by E6, FUNCT_1:def 12;
hence not verum by E4, E6, XBOOLE_0:3;
end;
then ( c4 in dom (c2 +* c3) & c2 . c4 = (c2 +* c3) . c4 ) by E6, FUNCT_4:12, FUNCT_4:13;
hence (c1 * (c2 +* c3)) . c4 = c1 . (c2 . c4) by FUNCT_1:23
.= (c1 * c2) . c4 by E6, FUNCT_1:23 ;

end;
hence c1 * (c2 +* c3) = c1 * c2 by E5, FUNCT_1:9;
end;

theorem E4: :: ALGSPEC1:4
for b1, b2, b3, b4 being Function holds
( ( b1 tolerates b2 & b3 tolerates b4 ) implies ( b1 * b3 tolerates b2 * b4 ) )
proof
let c1, c2, c3, c4 be Function;
assume that
E5: for b1 being set holds
( b1 in (dom c1) /\ (dom c2) implies c1 . b1 = c2 . b1 ) and
E6: for b1 being set holds
( b1 in (dom c3) /\ (dom c4) implies c3 . b1 = c4 . b1 ) ; :: according to PARTFUN1:def 6
let c5 be set ; :: according to PARTFUN1:def 6
assume c5 in (dom (c1 * c3)) /\ (dom (c2 * c4)) ;
then ( c5 in dom (c1 * c3) & c5 in dom (c2 * c4) ) by XBOOLE_0:def 3;
then E7: ( c5 in dom c3 & c3 . c5 in dom c1 & c5 in dom c4 & c4 . c5 in dom c2 ) by FUNCT_1:21;
then c5 in (dom c3) /\ (dom c4) by XBOOLE_0:def 3;
then E8: c3 . c5 = c4 . c5 by E6;
then ( c3 . c5 in (dom c1) /\ (dom c2) & (c1 * c3) . c5 = c1 . (c3 . c5) & (c2 * c4) . c5 = c2 . (c4 . c5) ) by E7, FUNCT_1:23, XBOOLE_0:def 3;
hence (c1 * c3) . c5 = (c2 * c4) . c5 by E5, E8;
end;

theorem E5: :: ALGSPEC1:5
for b1, b2, b3, b4 being non empty set
for b5 being Function of b1,b3
for b6 being Function of b2,b4 holds
( b5 c= b6 implies b5 * c= b6 * )
proof
let c1, c2, c3, c4 be non empty set ;
let c5 be Function of c1,c3;
let c6 be Function of c2,c4;
E6: ( dom c5 = c1 & dom c6 = c2 & dom (c5 * ) = c1 * & dom (c6 * ) = c2 * ) by FUNCT_2:def 1;
assume E7: c5 c= c6 ;
then dom c5 c= dom c6 by RELAT_1:25;
then E8: c1 * c= c2 * by E6, FINSEQ_1:83;
now
let c7 be set ;
assume c7 in c1 * ;
then reconsider c8 = c7 as Element of c1 * ;
(rng c8) /\ c2 c= rng c8 by XBOOLE_1:17;
then ( (rng c8) /\ c2 c= c1 & c8 in c1 * ) by XBOOLE_1:1;
then ( (c5 * ) . c8 = c5 * c8 & c8 in c2 * & c5 * c8 = c6 * c8 ) by E6, E7, E8, E2, LANG1:def 14;
hence (c5 * ) . c7 = (c6 * ) . c7 by LANG1:def 14;
end;
hence c5 * c= c6 * by E6, E8, GRFUNC_1:8;
end;

theorem E6: :: ALGSPEC1:6
for b1, b2, b3, b4 being non empty set
for b5 being Function of b1,b3
for b6 being Function of b2,b4 holds
( b5 tolerates b6 implies b5 * tolerates b6 * )
proof
let c1, c2, c3, c4 be non empty set ;
let c5 be Function of c1,c3;
let c6 be Function of c2,c4;
E7: ( dom c5 = c1 & dom c6 = c2 & dom (c5 * ) = c1 * & dom (c6 * ) = c2 * ) by FUNCT_2:def 1;
assume E8: for b1 being set holds
( b1 in (dom c5) /\ (dom c6) implies c5 . b1 = c6 . b1 ) ; :: according to PARTFUN1:def 6
let c7 be set ; :: according to PARTFUN1:def 6
assume c7 in (dom (c5 * )) /\ (dom (c6 * )) ;
then E9: ( c7 in dom (c5 * ) & c7 in dom (c6 * ) ) by XBOOLE_0:def 3;
then reconsider c8 = c7 as Element of c1 * ;
reconsider c9 = c7 as Element of c2 * by E9;
E10: ( (c5 * ) . c7 = c5 * c8 & (c6 * ) . c7 = c6 * c9 ) by LANG1:def 14;
( rng c8 c= c1 & rng c9 c= c2 ) ;
then E11: ( dom (c5 * c8) = dom c8 & dom (c6 * c9) = dom c9 ) by E7, RELAT_1:46;
now
let c10 be set ;
assume E12: c10 in dom c8 ;
then ( c8 . c10 in rng c8 & c9 . c10 in rng c9 ) by FUNCT_1:def 5;
then c8 . c10 in (dom c5) /\ (dom c6) by E7, XBOOLE_0:def 3;
then c5 . (c8 . c10) = c6 . (c9 . c10) by E8
.= (c6 * c9) . c10 by E12, FUNCT_1:23 ;
hence (c5 * c8) . c10 = (c6 * c9) . c10 by E12, FUNCT_1:23;
end;
hence (c5 * ) . c7 = (c6 * ) . c7 by E10, E11, FUNCT_1:9;
end;

definition
let c1 be set ;
let c2 be Function;
func c1 -indexing c2 -> ManySortedSet of a1 equals :: ALGSPEC1:def 1
(id a1) +* (a2 | a1);
coherence
(id c1) +* (c2 | c1) is ManySortedSet of c1
proof
dom (id c1) = c1 by RELAT_1:71;
then ( dom ((id c1) +* (c2 | c1)) = c1 \/ (dom (c2 | c1)) & dom (c2 | c1) c= c1 ) by FUNCT_4:def 1, RELAT_1:87;
then dom ((id c1) +* (c2 | c1)) = c1 by XBOOLE_1:12;
hence (id c1) +* (c2 | c1) is ManySortedSet of c1 by PBOOLE:def 3;
end;
end;

:: deftheorem defines -indexing ALGSPEC1:def 1 :
for b1 being set
for b2 being Function holds b1 -indexing b2 = (id b1) +* (b2 | b1);

theorem E7: :: ALGSPEC1:7
for b1 being set
for b2 being Function holds rng (b1 -indexing b2) = (b1 \ (dom b2)) \/ (b2 .: b1)
proof
let c1 be set ;
let c2 be Function;
E8: c1 \ (dom (c2 | c1)) c= c1 by XBOOLE_1:36;
( c1 -indexing c2 = (id c1) +* (c2 | c1) & dom (id c1) = c1 ) by RELAT_1:71;
hence rng (c1 -indexing c2) = ((id c1) .: (c1 \ (dom (c2 | c1)))) \/ (rng (c2 | c1)) by FRECHET:12
.= ((id c1) .: (c1 \ (dom (c2 | c1)))) \/ (c2 .: c1) by RELAT_1:148
.= (c1 \ (dom (c2 | c1))) \/ (c2 .: c1) by E8, FUNCT_1:162
.= (c1 \ ((dom c2) /\ c1)) \/ (c2 .: c1) by RELAT_1:90
.= (c1 \ (dom c2)) \/ (c2 .: c1) by XBOOLE_1:47 ;

end;

theorem E8: :: ALGSPEC1:8
for b1 being non empty set
for b2 being Function
for b3 being Element of b1 holds (b1 -indexing b2) . b3 = ((id b1) +* b2) . b3
proof
let c1 be non empty set ;
let c2 be Function;
let c3 be Element of c1;
((id c1) +* c2) | c1 = ((id c1) | c1) +* (c2 | c1) by FUNCT_4:75
.= ((id c1) | (dom (id c1))) +* (c2 | c1) by RELAT_1:71
.= (id c1) +* (c2 | c1) by RELAT_1:98
.= c1 -indexing c2 ;
hence (c1 -indexing c2) . c3 = ((id c1) +* c2) . c3 by FUNCT_1:72;
end;

theorem E9: :: ALGSPEC1:9
for b1, b2 being set
for b3 being Function holds
( b2 in b1 implies ( ( b2 in dom b3 implies (b1 -indexing b3) . b2 = b3 . b2 ) & ( not b2 in dom b3 implies (b1 -indexing b3) . b2 = b2 ) ) )
proof
let c1, c2 be set ;
let c3 be Function;
assume c2 in c1 ;
then ( (c1 -indexing c3) . c2 = ((id c1) +* c3) . c2 & dom (id c1) = c1 & (id c1) . c2 = c2 ) by E8, FUNCT_1:35, RELAT_1:71;
hence ( ( c2 in dom c3 implies (c1 -indexing c3) . c2 = c3 . c2 ) & ( not c2 in dom c3 implies (c1 -indexing c3) . c2 = c2 ) ) by FUNCT_4:12, FUNCT_4:14;
end;

theorem E10: :: ALGSPEC1:10
for b1 being set
for b2 being Function holds
( dom b2 = b1 implies b1 -indexing b2 = b2 )
proof
let c1 be set ;
let c2 be Function;
assume E11: dom c2 = c1 ;
then ( c2 | c1 = c2 & dom (id c1) = c1 & c1 -indexing c2 = (id c1) +* (c2 | c1) ) by RELAT_1:71, RELAT_1:97;
hence c1 -indexing c2 = c2 by E11, FUNCT_4:20;
end;

theorem E11: :: ALGSPEC1:11
for b1 being set
for b2 being Function holds b1 -indexing (b1 -indexing b2) = b1 -indexing b2
proof
let c1 be set ;
let c2 be Function;
dom (c1 -indexing c2) = c1 by PBOOLE:def 3;
then for b1 being set holds
( b1 in c1 implies (c1 -indexing (c1 -indexing c2)) . b1 = (c1 -indexing c2) . b1 ) by E9;
hence c1 -indexing (c1 -indexing c2) = c1 -indexing c2 by PBOOLE:3;
end;

theorem E12: :: ALGSPEC1:12
for b1 being set
for b2 being Function holds b1 -indexing ((id b1) +* b2) = b1 -indexing b2
proof
let c1 be set ;
let c2 be Function;
E13: dom (id c1) = c1 by RELAT_1:71;
thus c1 -indexing ((id c1) +* c2) = (id c1) +* (((id c1) +* c2) | c1)
.= (id c1) +* (((id c1) | c1) +* (c2 | c1)) by FUNCT_4:75
.= (id c1) +* ((id c1) +* (c2 | c1)) by E13, RELAT_1:97
.= ((id c1) +* (id c1)) +* (c2 | c1) by FUNCT_4:15
.= c1 -indexing c2 ;
end;

theorem E13: :: ALGSPEC1:13
for b1 being set
for b2 being Function holds
( b2 c= id b1 implies b1 -indexing b2 = id b1 )
proof
let c1 be set ;
let c2 be Function;
E14: dom (id c1) = c1 by RELAT_1:71;
assume c2 c= id c1 ;
then (id c1) +* c2 = id c1 by FUNCT_4:79;
hence c1 -indexing c2 = c1 -indexing (id c1) by E12
.= id c1 by E14, E10 ;

end;

theorem :: ALGSPEC1:14
for b1 being set holds b1 -indexing {} = id b1
proof
let c1 be set ;
{} c= id c1 by XBOOLE_1:2;
hence c1 -indexing {} = id c1 by E13;
end;

theorem E14: :: ALGSPEC1:15
for b1 being set
for b2 being Function holds b1 -indexing (b2 | b1) = b1 -indexing b2 by RELAT_1:101;

theorem E15: :: ALGSPEC1:16
for b1 being set
for b2 being Function holds
( b1 c= dom b2 implies b1 -indexing b2 = b2 | b1 )
proof
let c1 be set ;
let c2 be Function;
assume c1 c= dom c2 ;
then E16: dom (c2 | c1) = c1 by RELAT_1:91;
thus c1 -indexing c2 = c1 -indexing (c2 | c1) by E14
.= c2 | c1 by E16, E10 ;
end;

theorem :: ALGSPEC1:17
for b1 being Function holds {} -indexing b1 = {}
proof
let c1 be Function;
{} c= dom c1 by XBOOLE_1:2;
hence {} -indexing c1 = c1 | {} by E15
.= {} by RELAT_1:110 ;

end;

theorem E16: :: ALGSPEC1:18
for b1, b2 being set
for b3 being Function holds
( b1 c= b2 implies (b2 -indexing b3) | b1 = b1 -indexing b3 )
proof
let c1, c2 be set ;
let c3 be Function;
assume c1 c= c2 ;
then ( (id c2) | c1 = id c1 & (c3 | c2) | c1 = c3 | c1 & c1 -indexing c3 = (id c1) +* (c3 | c1) & c2 -indexing c3 = (id c2) +* (c3 | c2) ) by FUNCT_3:1, RELAT_1:103;
hence (c2 -indexing c3) | c1 = c1 -indexing c3 by FUNCT_4:75;
end;

theorem E17: :: ALGSPEC1:19
for b1, b2 being set
for b3 being Function holds (b1 \/ b2) -indexing b3 = (b1 -indexing b3) +* (b2 -indexing b3)
proof
let c1, c2 be set ;
let c3 be Function;
set c4 = c1 \/ c2;
( c3 | c1 c= c3 & c3 | c2 c= c3 ) by RELAT_1:88;
then c3 | c1 tolerates c3 | c2 by PARTFUN1:131;
then E18: (c3 | c1) \/ (c3 | c2) = (c3 | c1) +* (c3 | c2) by FUNCT_4:31;
E19: ( dom (c3 | c1) = (dom c3) /\ c1 & dom (c3 | c2) = (dom c3) /\ c2 ) by RELAT_1:90;
then ( dom (c3 | c1) c= dom c3 & dom (id c2) c= c2 ) by XBOOLE_1:17;
then E20: (dom (c3 | c1)) /\ (dom (id c2)) c= dom (c3 | c2) by E19, XBOOLE_1:27;
thus (c1 \/ c2) -indexing c3 = (id (c1 \/ c2)) +* (c3 | (c1 \/ c2))
.= ((id c1) +* (id c2)) +* (c3 | (c1 \/ c2)) by FUNCT_4:23
.= ((id c1) +* (id c2)) +* ((c3 | c1) +* (c3 | c2)) by E18, RELAT_1:107
.= (id c1) +* ((id c2) +* ((c3 | c1) +* (c3 | c2))) by FUNCT_4:15
.= (id c1) +* (((id c2) +* (c3 | c1)) +* (c3 | c2)) by FUNCT_4:15
.= (id c1) +* (((c3 | c1) +* (id c2)) +* (c3 | c2)) by E20, E1
.= (id c1) +* ((c3 | c1) +* ((id c2) +* (c3 | c2))) by FUNCT_4:15
.= ((id c1) +* (c3 | c1)) +* ((id c2) +* (c3 | c2)) by FUNCT_4:15
.= (c1 -indexing c3) +* ((id c2) +* (c3 | c2))
.= (c1 -indexing c3) +* (c2 -indexing c3) ;
end;

theorem E18: :: ALGSPEC1:20
for b1, b2 being set
for b3 being Function holds b1 -indexing b3 tolerates b2 -indexing b3
proof
let c1, c2 be set ;
let c3 be Function;
( c1 c= c1 \/ c2 & c2 c= c1 \/ c2 ) by XBOOLE_1:7;
then ( c1 -indexing c3 = ((c1 \/ c2) -indexing c3) | c1 & c2 -indexing c3 = ((c1 \/ c2) -indexing c3) | c2 ) by E16;
then ( c1 -indexing c3 c= (c1 \/ c2) -indexing c3 & c2 -indexing c3 c= (c1 \/ c2) -indexing c3 ) by RELAT_1:88;
hence c1 -indexing c3 tolerates c2 -indexing c3 by PARTFUN1:131;
end;

theorem E19: :: ALGSPEC1:21
for b1, b2 being set
for b3 being Function holds (b1 \/ b2) -indexing b3 = (b1 -indexing b3) \/ (b2 -indexing b3)
proof
let c1, c2 be set ;
let c3 be Function;
( (c1 \/ c2) -indexing c3 = (c1 -indexing c3) +* (c2 -indexing c3) & c1 -indexing c3 tolerates c2 -indexing c3 ) by E17, E18;
hence (c1 \/ c2) -indexing c3 = (c1 -indexing c3) \/ (c2 -indexing c3) by FUNCT_4:31;
end;

theorem E20: :: ALGSPEC1:22
for b1 being non empty set
for b2, b3 being Function holds
( rng b3 c= b1 implies (b1 -indexing b2) * b3 = ((id b1) +* b2) * b3 )
proof
let c1 be non empty set ;
let c2, c3 be Function;
assume E21: rng c3 c= c1 ;
dom (id c1) = c1 by RELAT_1:71;
then ( dom ((id c1) +* c2) = c1 \/ (dom c2) & c1 c= c1 \/ (dom c2) ) by FUNCT_4:def 1, XBOOLE_1:7;
then ( rng c3 c= dom (c1 -indexing c2) & rng c3 c= dom ((id c1) +* c2) ) by E21, PBOOLE:def 3, XBOOLE_1:1;
then E22: ( dom ((c1 -indexing c2) * c3) = dom c3 & dom (((id c1) +* c2) * c3) = dom c3 ) by RELAT_1:46;
now
let c4 be set ;
assume c4 in dom c3 ;
then ( ((c1 -indexing c2) * c3) . c4 = (c1 -indexing c2) . (c3 . c4) & (((id c1) +* c2) * c3) . c4 = ((id c1) +* c2) . (c3 . c4) & c3 . c4 in rng c3 ) by FUNCT_1:23, FUNCT_1:def 5;
hence ((c1 -indexing c2) * c3) . c4 = (((id c1) +* c2) * c3) . c4 by E21, E8;
end;
hence (c1 -indexing c2) * c3 = ((id c1) +* c2) * c3 by E22, FUNCT_1:9;
end;

theorem :: ALGSPEC1:23
for b1, b2 being Function holds
( ( dom b1 misses dom b2 & rng b2 misses dom b1 ) implies ( ( for b3 being set holds b1 * (b3 -indexing b2) = b1 | b3 ) ) )
proof
let c1, c2 be Function;
assume E21: ( dom c1 misses dom c2 & rng c2 misses dom c1 ) ;
let c3 be set ;
E22: c1 | c3 c= c1 by RELAT_1:88;
E23: ( dom (c1 | c3) c= c3 & dom (id c3) = c3 & rng (id c3) = c3 ) by RELAT_1:71, RELAT_1:87;
( dom (c1 | c3) c= dom c1 & dom (c2 | c3) c= dom c2 & rng (c2 | c3) c= rng c2 ) by RELAT_1:89, RELAT_1:99;
then E24: ( dom (c1 | c3) misses rng (c2 | c3) & dom (c1 | c3) misses dom (c2 | c3) ) by E21, XBOOLE_1:64;
(id c3) .: (dom (c2 | c3)) c= dom (c2 | c3)
proof
let c4 be set ; :: according to TARSKI:def 3
assume c4 in (id c3) .: (dom (c2 | c3)) ;
then consider c5 being set such that
E25: ( c5 in dom (id c3) & c5 in dom (c2 | c3) & c4 = (id c3) . c5 ) by FUNCT_1:def 12;
thus c4 in dom (c2 | c3) by E25, FUNCT_1:35;
end;
then E25: (id c3) .: (dom (c2 | c3)) misses dom (c1 | c3) by E24, XBOOLE_1:64;
c2 .: c3 c= rng c2 by RELAT_1:144;
then c2 .: c3 misses dom c1 by E21, XBOOLE_1:64;
then E26: (c2 .: c3) /\ (dom c1) = {} by XBOOLE_0:def 7;
E27: c3 \ (dom c2) c= c3 by XBOOLE_1:36;
rng (c3 -indexing c2) = (c3 \ (dom c2)) \/ (c2 .: c3) by E7;
then (rng (c3 -indexing c2)) /\ (dom c1) = ((c3 \ (dom c2)) /\ (dom c1)) \/ ((c2 .: c3) /\ (dom c1)) by XBOOLE_1:23
.= (c3 \ (dom c2)) /\ (dom c1) by E26 ;
then (rng (c3 -indexing c2)) /\ (dom c1) c= c3 /\ (dom c1) by E27, XBOOLE_1:26;
then (rng (c3 -indexing c2)) /\ (dom c1) c= dom (c1 | c3) by RELAT_1:90;
hence c1 * (c3 -indexing c2) = (c1 | c3) * (c3 -indexing c2) by E22, E2
.= (c1 | c3) * ((id c3) +* (c2 | c3))
.= (c1 | c3) * (id c3) by E23, E24, E25, E3
.= c1 | c3 by E23, RELAT_1:77 ;

end;

definition
let c1 be Function;
mode rng-retract of c1 -> Function means :E21: :: ALGSPEC1:def 2
( dom a2 = rng a1 & a1 * a2 = id (rng a1) );
existence
ex b1 being Function st
( dom b1 = rng c1 & c1 * b1 = id (rng c1) )
proof
defpred S1[ set , set ] means c1 . a2 = a1;
E21: for b1 being set holds
not ( b1 in rng c1 & ( for b2 being set holds
not ( b2 in dom c1 & S1[b1,b2] ) ) ) by FUNCT_1:def 5;
consider c2 being Function such that
E22: ( dom c2 = rng c1 & rng c2 c= dom c1 ) and
E23: for b1 being set holds
( b1 in rng c1 implies S1[b1,c2 . b1] ) from WELLORD2:sch 1(E21);
 take c2 ;
thus dom c2 = rng c1 by E22;
E24: dom (c1 * c2) = rng c1 by E22, RELAT_1:46;
E25: dom (id (rng c1)) = rng c1 by RELAT_1:71;
now
let c3 be set ;
assume E26: c3 in rng c1 ;
then ( c1 . (c2 . c3) = c3 & (c1 * c2) . c3 = c1 . (c2 . c3) ) by E22, E23, FUNCT_1:23;
hence (c1 * c2) . c3 = (id (rng c1)) . c3 by E26, FUNCT_1:35;
end;
hence c1 * c2 = id (rng c1) by E24, E25, FUNCT_1:9;
end;
end;

:: deftheorem E21 defines rng-retract ALGSPEC1:def 2 :
for b1, b2 being Function holds
( b2 is rng-retract of b1 iff ( dom b2 = rng b1 & b1 * b2 = id (rng b1) ) );

theorem E22: :: ALGSPEC1:24
for b1 being Function
for b2 being rng-retract of b1 holds rng b2 c= dom b1
proof
let c1, c2 be Function;
assume ( dom c2 = rng c1 & c1 * c2 = id (rng c1) ) ; :: according to ALGSPEC1:def 2
then dom c2 = dom (c1 * c2) by RELAT_1:71;
hence rng c2 c= dom c1 by FUNCT_1:27;
end;

theorem E23: :: ALGSPEC1:25
for b1 being Function
for b2 being rng-retract of b1
for b3 being set holds
( b3 in rng b1 implies ( b2 . b3 in dom b1 & b1 . (b2 . b3) = b3 ) )
proof
let c1 be Function;
let c2 be rng-retract of c1;
let c3 be set ;
assume E24: c3 in rng c1 ;
E25: dom c2 = rng c1 by E21;
then ( c2 . c3 in rng c2 & rng c2 c= dom c1 ) by E24, E22, FUNCT_1:def 5;
hence c2 . c3 in dom c1 ;
thus c1 . (c2 . c3) = (c1 * c2) . c3 by E24, E25,