let f1, f2, f3 be FinSequence; :: thesis: ( f1 c= f2 implies f3 ^ f1 c= f3 ^ f2 )
assume A1: f1 c= f2 ; :: thesis: f3 ^ f1 c= f3 ^ f2
A2: dom (f3 ^ f1) c= dom (f3 ^ f2)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f3 ^ f1) or x in dom (f3 ^ f2) )
assume A3: x in dom (f3 ^ f1) ; :: thesis: x in dom (f3 ^ f2)
then reconsider i = x as Nat ;
per cases ( i in dom f3 or ex n being Nat st
( n in dom f1 & i = (len f3) + n ) ) by A3, FINSEQ_1:25;
suppose A4: i in dom f3 ; :: thesis: x in dom (f3 ^ f2)
dom f3 c= dom (f3 ^ f2) by FINSEQ_1:26;
hence x in dom (f3 ^ f2) by A4; :: thesis: verum
end;
suppose A5: ex n being Nat st
( n in dom f1 & i = (len f3) + n ) ; :: thesis: x in dom (f3 ^ f2)
dom f1 c= dom f2 by A1, RELAT_1:11;
hence x in dom (f3 ^ f2) by A5, FINSEQ_1:28; :: thesis: verum
end;
end;
end;
for x being object st x in dom (f3 ^ f1) holds
(f3 ^ f1) . x = (f3 ^ f2) . x
proof
let x be object ; :: thesis: ( x in dom (f3 ^ f1) implies (f3 ^ f1) . x = (f3 ^ f2) . x )
assume A6: x in dom (f3 ^ f1) ; :: thesis: (f3 ^ f1) . x = (f3 ^ f2) . x
then reconsider i = x as Nat ;
per cases ( i in dom f3 or ex n being Nat st
( n in dom f1 & i = (len f3) + n ) ) by A6, FINSEQ_1:25;
suppose A7: i in dom f3 ; :: thesis: (f3 ^ f1) . x = (f3 ^ f2) . x
hence (f3 ^ f1) . x = f3 . i by FINSEQ_1:def 7
.= (f3 ^ f2) . x by A7, FINSEQ_1:def 7 ;
:: thesis: verum
end;
suppose A8: ex n being Nat st
( n in dom f1 & i = (len f3) + n ) ; :: thesis: (f3 ^ f1) . x = (f3 ^ f2) . x
A9: dom f1 c= dom f2 by A1, RELAT_1:11;
consider k being Nat such that
A10: k in dom f1 and
A11: i = (len f3) + k by A8;
thus (f3 ^ f1) . x = f1 . k by A10, A11, FINSEQ_1:def 7
.= f2 . k by A1, A10, GRFUNC_1:2
.= (f3 ^ f2) . x by A10, A11, A9, FINSEQ_1:def 7 ; :: thesis: verum
end;
end;
end;
hence f3 ^ f1 c= f3 ^ f2 by A2, GRFUNC_1:2; :: thesis: verum