let X, Y be set ; :: thesis: for k being Nat st X c= Seg k & Y c= dom (Sgm X) holds

(Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))

let k be Nat; :: thesis: ( X c= Seg k & Y c= dom (Sgm X) implies (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y)) )

assume that

A1: X c= Seg k and

A2: Y c= dom (Sgm X) ; :: thesis: (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))

reconsider Y9 = Y as finite set by A2;

set M = (Sgm X) * (Sgm Y);

set R = rng ((Sgm X) | Y);

A3: Y c= Seg (len (Sgm X)) by A2, FINSEQ_1:def 3;

then A4: rng (Sgm Y) = Y by FINSEQ_1:def 13;

dom (Sgm Y9) = Seg (card Y9) by A3, FINSEQ_3:40;

then A5: dom ((Sgm X) * (Sgm Y)) = Seg (card Y9) by A2, A4, RELAT_1:27;

A6: rng (Sgm X) c= Seg k by A1, FINSEQ_1:def 13;

then A7: rng (Sgm X) c= NAT by XBOOLE_1:1;

reconsider M = (Sgm X) * (Sgm Y) as FinSequence by A5, FINSEQ_1:def 2;

rng M c= rng (Sgm X) by RELAT_1:26;

then rng M c= NAT by A7;

then reconsider L = (Sgm X) * (Sgm Y) as FinSequence of NAT by FINSEQ_1:def 4;

then rng ((Sgm X) | Y) c= Seg k by A6;

hence (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y)) by A18, A19, FINSEQ_1:def 13; :: thesis: verum

(Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))

let k be Nat; :: thesis: ( X c= Seg k & Y c= dom (Sgm X) implies (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y)) )

assume that

A1: X c= Seg k and

A2: Y c= dom (Sgm X) ; :: thesis: (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))

reconsider Y9 = Y as finite set by A2;

set M = (Sgm X) * (Sgm Y);

set R = rng ((Sgm X) | Y);

A3: Y c= Seg (len (Sgm X)) by A2, FINSEQ_1:def 3;

then A4: rng (Sgm Y) = Y by FINSEQ_1:def 13;

dom (Sgm Y9) = Seg (card Y9) by A3, FINSEQ_3:40;

then A5: dom ((Sgm X) * (Sgm Y)) = Seg (card Y9) by A2, A4, RELAT_1:27;

A6: rng (Sgm X) c= Seg k by A1, FINSEQ_1:def 13;

then A7: rng (Sgm X) c= NAT by XBOOLE_1:1;

reconsider M = (Sgm X) * (Sgm Y) as FinSequence by A5, FINSEQ_1:def 2;

rng M c= rng (Sgm X) by RELAT_1:26;

then rng M c= NAT by A7;

then reconsider L = (Sgm X) * (Sgm Y) as FinSequence of NAT by FINSEQ_1:def 4;

now :: thesis: for y being object holds

( ( y in rng L implies y in rng ((Sgm X) | Y) ) & ( y in rng ((Sgm X) | Y) implies y in rng L ) )

then A18:
rng L = rng ((Sgm X) | Y)
by TARSKI:2;( ( y in rng L implies y in rng ((Sgm X) | Y) ) & ( y in rng ((Sgm X) | Y) implies y in rng L ) )

let y be object ; :: thesis: ( ( y in rng L implies y in rng ((Sgm X) | Y) ) & ( y in rng ((Sgm X) | Y) implies y in rng L ) )

then consider x being object such that

A11: x in dom ((Sgm X) | Y) and

A12: y = ((Sgm X) | Y) . x by FUNCT_1:def 3;

A13: x in (dom (Sgm X)) /\ Y by A11, RELAT_1:61;

then A14: x in Y by XBOOLE_0:def 4;

then consider z being object such that

A15: z in dom (Sgm Y) and

A16: x = (Sgm Y) . z by A4, FUNCT_1:def 3;

x in dom (Sgm X) by A13, XBOOLE_0:def 4;

then A17: z in dom ((Sgm X) * (Sgm Y)) by A15, A16, FUNCT_1:11;

y = (Sgm X) . x by A12, A14, FUNCT_1:49;

then L . z = y by A16, A17, FUNCT_1:12;

hence y in rng L by A17, FUNCT_1:def 3; :: thesis: verum

end;hereby :: thesis: ( y in rng ((Sgm X) | Y) implies y in rng L )

assume
y in rng ((Sgm X) | Y)
; :: thesis: y in rng Lassume
y in rng L
; :: thesis: y in rng ((Sgm X) | Y)

then consider x being object such that

A8: x in dom L and

A9: y = L . x by FUNCT_1:def 3;

x in dom (Sgm Y) by A8, FUNCT_1:11;

then A10: (Sgm Y) . x in Y by A4, FUNCT_1:def 3;

y = (Sgm X) . ((Sgm Y) . x) by A8, A9, FUNCT_1:12;

hence y in rng ((Sgm X) | Y) by A2, A10, FUNCT_1:50; :: thesis: verum

end;then consider x being object such that

A8: x in dom L and

A9: y = L . x by FUNCT_1:def 3;

x in dom (Sgm Y) by A8, FUNCT_1:11;

then A10: (Sgm Y) . x in Y by A4, FUNCT_1:def 3;

y = (Sgm X) . ((Sgm Y) . x) by A8, A9, FUNCT_1:12;

hence y in rng ((Sgm X) | Y) by A2, A10, FUNCT_1:50; :: thesis: verum

then consider x being object such that

A11: x in dom ((Sgm X) | Y) and

A12: y = ((Sgm X) | Y) . x by FUNCT_1:def 3;

A13: x in (dom (Sgm X)) /\ Y by A11, RELAT_1:61;

then A14: x in Y by XBOOLE_0:def 4;

then consider z being object such that

A15: z in dom (Sgm Y) and

A16: x = (Sgm Y) . z by A4, FUNCT_1:def 3;

x in dom (Sgm X) by A13, XBOOLE_0:def 4;

then A17: z in dom ((Sgm X) * (Sgm Y)) by A15, A16, FUNCT_1:11;

y = (Sgm X) . x by A12, A14, FUNCT_1:49;

then L . z = y by A16, A17, FUNCT_1:12;

hence y in rng L by A17, FUNCT_1:def 3; :: thesis: verum

A19: now :: thesis: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len L & k1 = L . l & k2 = L . m holds

k1 < k2

rng ((Sgm X) | Y) c= rng (Sgm X)
by RELAT_1:70;k1 < k2

let l, m, k1, k2 be Nat; :: thesis: ( 1 <= l & l < m & m <= len L & k1 = L . l & k2 = L . m implies k1 < k2 )

assume that

A20: 1 <= l and

A21: l < m and

A22: m <= len L and

A23: k1 = L . l and

A24: k2 = L . m ; :: thesis: k1 < k2

l <= len L by A21, A22, XXREAL_0:2;

then A25: l in dom L by A20, FINSEQ_3:25;

then A26: L . l = (Sgm X) . ((Sgm Y) . l) by FUNCT_1:12;

1 <= m by A20, A21, XXREAL_0:2;

then A27: m in dom L by A22, FINSEQ_3:25;

then A28: L . m = (Sgm X) . ((Sgm Y) . m) by FUNCT_1:12;

A29: (Sgm Y) . l in dom (Sgm X) by A25, FUNCT_1:11;

m in dom (Sgm Y) by A27, FUNCT_1:11;

then A30: m <= len (Sgm Y) by FINSEQ_3:25;

A31: (Sgm Y) . m in dom (Sgm X) by A27, FUNCT_1:11;

reconsider l = l, m = m as Element of NAT by ORDINAL1:def 12;

reconsider K1 = (Sgm Y) . l, K2 = (Sgm Y) . m as Element of NAT by ORDINAL1:def 12;

A32: 1 <= K1 by A29, FINSEQ_3:25;

A33: K2 <= len (Sgm X) by A31, FINSEQ_3:25;

K1 < K2 by A3, A20, A21, A30, FINSEQ_1:def 13;

hence k1 < k2 by A1, A23, A24, A26, A28, A32, A33, FINSEQ_1:def 13; :: thesis: verum

end;assume that

A20: 1 <= l and

A21: l < m and

A22: m <= len L and

A23: k1 = L . l and

A24: k2 = L . m ; :: thesis: k1 < k2

l <= len L by A21, A22, XXREAL_0:2;

then A25: l in dom L by A20, FINSEQ_3:25;

then A26: L . l = (Sgm X) . ((Sgm Y) . l) by FUNCT_1:12;

1 <= m by A20, A21, XXREAL_0:2;

then A27: m in dom L by A22, FINSEQ_3:25;

then A28: L . m = (Sgm X) . ((Sgm Y) . m) by FUNCT_1:12;

A29: (Sgm Y) . l in dom (Sgm X) by A25, FUNCT_1:11;

m in dom (Sgm Y) by A27, FUNCT_1:11;

then A30: m <= len (Sgm Y) by FINSEQ_3:25;

A31: (Sgm Y) . m in dom (Sgm X) by A27, FUNCT_1:11;

reconsider l = l, m = m as Element of NAT by ORDINAL1:def 12;

reconsider K1 = (Sgm Y) . l, K2 = (Sgm Y) . m as Element of NAT by ORDINAL1:def 12;

A32: 1 <= K1 by A29, FINSEQ_3:25;

A33: K2 <= len (Sgm X) by A31, FINSEQ_3:25;

K1 < K2 by A3, A20, A21, A30, FINSEQ_1:def 13;

hence k1 < k2 by A1, A23, A24, A26, A28, A32, A33, FINSEQ_1:def 13; :: thesis: verum

then rng ((Sgm X) | Y) c= Seg k by A6;

hence (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y)) by A18, A19, FINSEQ_1:def 13; :: thesis: verum