let S, T be non empty RelStr ; :: thesis: for s being Element of S
for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) ` ),the carrier of T:] \/ [:the carrier of S,((uparrow t) ` ):]
let s be Element of S; :: thesis: for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) ` ),the carrier of T:] \/ [:the carrier of S,((uparrow t) ` ):]
let t be Element of T; :: thesis: (uparrow [s,t]) ` = [:((uparrow s) ` ),the carrier of T:] \/ [:the carrier of S,((uparrow t) ` ):]
thus (uparrow [s,t]) ` = [:the carrier of S,the carrier of T:] \ (uparrow [s,t]) by YELLOW_3:def 2
.= [:the carrier of S,the carrier of T:] \ [:(uparrow s),(uparrow t):] by YELLOW10:40
.= [:((uparrow s) ` ),the carrier of T:] \/ [:the carrier of S,((uparrow t) ` ):] by ZFMISC_1:126 ; :: thesis: verum